package tr.edu.ege.kipler.satisfiability;

import java.util.Set;

import tr.edu.ege.kipler.satisfiability.completion.rules.nondeterminism.BranchingPoint;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.satisfiability.profile.ReasoningProfile;
import tr.edu.ege.kipler.syntax.WorldElement;

/**
 * This is the generic reasoner interface. It provides a public interface to the
 * tableau algorithm. It supports two main operations which are satisfiability
 * checking of a set of formulas, and determining whether a given formula is
 * logically inferred from a set of formulas.
 * 
 * @author İnanç Seylan
 */
public interface Reasoner {
	/**
	 * Adds a formula to the knowledge base.
	 * 
	 * @param formula
	 */
	public void addFormula(WorldElement formula);

	/**
	 * Adds a set of formulas to the knowledge base.
	 * 
	 * @param formulas
	 */
	public void addFormulas(Set<WorldElement> formulas);

	/**
	 * 
	 * @return true if the knowledge base is satisfiable.
	 * @throws Exception
	 */
	public boolean isSatisfiable() throws Exception;

	/**
	 * @param formula
	 * @return true if the given formula can logically be inferred from the
	 *         knowledge base.
	 * @throws Exception
	 */
	public boolean isLogicalConsequence(WorldElement formula) throws Exception;

	/**
	 * Tells the reasoner to add a branching point for a possible backtracking.
	 * 
	 * @param bp
	 */
	public void addBranch(BranchingPoint bp);

	/**
	 * @return the active {@link WorldConstraintSystem}.
	 */
	public WorldConstraintSystem getCurrentWcs();

	/**
	 * @return the set of options that the reasoner uses.
	 */
	public ReasoningProfile getProfile();
}
